;(set-option :produce-proofs true)
(set-option :produce-interpolants true)
(set-logic QF_LRA)
(declare-fun |state_type::state.x| () Real)
(declare-fun |state_type::state.y| () Real)
(declare-fun |state_type::state.z| () Real)
(assert (! (let ((l0 (/ 9 10))) (let ((l1 (- l0))) (let ((l2 (= |state_type::state.x| l1))) (let ((l3 (= |state_type::state.y| 0))) (let ((l4 (= |state_type::state.z| l0))) (let ((l5 (and l2 l3 l4))) l5)))))) :named p1))
(push 1)
(assert (! (let ((l0 (* (/ (- 104647) 164745) |state_type::state.x|))) (let ((l1 (* (/ (- 19666) 128135) |state_type::state.y|))) (let ((l2 (* (/ 105892 230643) |state_type::state.z|))) (let ((l3 (+ (/ (- 35559) 36610) l0 l1 l2))) (let ((l4 (>= l3 0))) (let ((l5 (not l4))) l5)))))) :named p6))
(check-sat)
(get-interpolants p1 p6)
(pop 1)
(push 1)
(assert (! (let ((l0 (* (/ (- 104647) 694575) |state_type::state.x|))) (let ((l1 (* (/ (- 19666) 540225) |state_type::state.y|))) (let ((l2 (* (/ 105892 972405) |state_type::state.z|))) (let ((l3 (+ (/ (- 81) 490) l0 l1 l2))) (let ((l4 (>= l3 0))) (let ((l5 (not l4))) l5)))))) :named p7))
(check-sat)
(get-interpolants p1 p7)
